\section{\label{sec:related}Related Work}
\label{sec:related}

\noindent\textbf{Static tools.}~Several static and dynamic race
detection tools have been previously proposed.  Static tools based on
dataflow
analysis~\cite{dwyer-clarke-fse94,flanagan-abadi-esop1999,boyapati-rinard-2001,agarwal-stoller-vmcai2004,naik-etal-pldi2006}
are typically fast and do not require the construction of test drivers
but can report many false alarms; they make conservative
assumptions\Comment{\footnote{For example, for a language with
    pointers (or references), assumptions about possible pointer
    locations and, for an object-oriented language, assumptions about
    the types of targets of method invocations.}} that accumulate,
leading to imprecision in error reports\Comment{ tend to result in a
  large number of false positives}.  Static tools based on pattern
matching such as FindBugs~\cite{findbugs-web-page} or
JLint~\cite{jlint-web-page} can in addition miss errors due to an
incomplete set of supported patterns.  Compared to static tools, the
warnings \tname{} reports are based on dynamic information and
therefore do not suffer from the same sources of imprecision.  Our
approach is complementary to static tools; it builds on model checkers
that require different inputs and provide different guarantees.

\vspace{1ex}\noindent\textbf{Space reduction techniques.}~Program
model checkers use, often lossy, space reduction
techniques~\cite{lerda:01,visser-etal-2005,MusuvathiQadeer2007} to
alleviate the high cost associated with state-space exploration.  The
opportunity of improvement of \tname{} is proportional to such high
cost.  Musuvathi and Qadeer~\cite{MusuvathiQadeer2007} recently
proposed CHESS to constrain the number of context switches that the
model checker performs during the state-space exploration.  They show
substantial gain in space reduction without practical loss in
capability of finding errors.  We plan to evaluate \tname{} with
CHESS-like search in the future.

\vspace{1ex}\noindent\textbf{Heuristic model checking.}~Heuristic
model checking has been investigated under different contexts in the
past~\cite{groce02:model,rungta-mercer-haifa2008}. Rungta and
Mercer~\cite{rungta-mercer-haifa2008} use the warnings produced by
tools such as FindBugs~\cite{findbugs-web-page} or
JLint~\cite{jlint-web-page} to drive state-space exploration.  Even
though it is possible to build on similar ideas to guide exploration
with \tname{}, this is orthogonal to our current goal.  Note that the
model checker can find many errors, not only races, for one arbitrary
search.  In principle, the use of \tname{} in such conditions would
\emph{not} interfere with the capability of the model checker in
finding those errors.

\vspace{1ex}\noindent\textbf{Predictive analysis.}~Predictive analysis
has recently gained force as a dynamic technique to find concurrency
errors~\cite{feng-chen-2008,sorrentino-fse2010}.  The typical approach
uses a representative schedule of the program (containing, for
instance, reads and writes to memory, lock acquires and releases,
etc.) and, from that, infers new schedules based on some criteria.
Different techniques vary in what they use to infer new schedules
(e.g., causal dependencies).  Considering that not all of the
schedules inferred are feasible in the program, some techniques, like
Penelope~\cite{sorrentino-fse2010}, execute the schedule to confirm
(or not) the fault.  Cost is associated with the construction of the
model to represent the space of possible schedules, the analysis of
the model (to produce schedules), and the execution (/confirmation) of
inferred schedules.  A distinct feature of \tname{} compared to
existing predictive analysis tools is that it uses information of
multiple execution traces and that it non-intrusively integrates with
a model checkers.  This allows the model checker to find other kinds
of errors like assertion violations or deadlocks in case the
application does not contain races.

\vspace{1ex}\noindent\textbf{Language support.}~New
methods~\cite{yi-ppopp2011} and language
support~\cite{larus-kozyrakis-cacm2008} have been recently proposed to
facilitate development of multithreaded software.  The approach of
\tname{} complements these initiatives in checking software that uses
the dominant shared-memory model of concurrent programming.

%% which often report higher ratios of false
%% alarms~\cite{luo-etal-scam2010}.


%% Dynamic
%% tools\Comment{~\cite{godefroid97:model,musuvathi02:cmc,visser03model,marino-etal-pldi2009,flanagan-freund-pldi2009}}
%% can be significantly slower compared to static tools and also miss
%% errors, however, they typically don't report false alarms.  


%% \Fix{Discuss high and low-level race detection.}

%% \Fix{revise this...}


%% Recently, Marino~\etal{}~\cite{marino-etal-pldi2009} realized that
%% sampling could be very helpful to speed-up detection of data-races.
%% They selectively monitor thread accesses based on data obtained with
%% profiling.  Even though their goal is different, their fundamental
%% idea is similar to ours.  They recognize that not all points of
%% execution deserve same attention.  



%% Previous dynamic analysis work focused on reducing cost of
%% instrumentation for efficient runtime
%% verification~\cite{schonberg-pldi1989,praun-gross-oopsla2001,pozniansky-schuster-2007,flanagan-freund-pldi2009,marino-etal-pldi2009},
%% and on improving precision of monitors~\cite{bodden-havelund-issta08}
%% that typically use variations of the Eraser lockset
%% algorithm~\cite{savage-etal-1997}.  These algorithms typically build
%% state machines too encode program states.  We remain to evaluate
%% whether \tname{} can leverage the distance to race states on these
%% state machines to adjust its measure of fitness.

%% \Fix{...Beverly Sanders work...}

%% \Fix{discuss race prediction analysis}

% LocalWords:  dataflow FindBugs JLint lossy Musuvathi Qadeer Rungta
% LocalWords:  interleavings multithreaded
